package br.ufrn.btest.decorators.predicates;

import java.util.ArrayList;
import java.util.List;
import java.util.Set;

import br.ufrn.btest.decorators.expressions.MyExpression;
import br.ufrn.btest.decorators.expressions.MyExpressionFactory;
import de.be4.classicalb.core.parser.node.AUniversalQuantificationPredicate;
import de.be4.classicalb.core.parser.node.PExpression;
import de.be4.classicalb.core.parser.node.PPredicate;

public class MyAUniversalQuantificationPredicate extends MyPredicateDecorator {
	
	
	private AUniversalQuantificationPredicate universalQuantification;

	
	
	public MyAUniversalQuantificationPredicate(
			AUniversalQuantificationPredicate universalQuantification) {
		this.universalQuantification = universalQuantification;
	}

	
	
	@Override
	public PPredicate getNode() {
		return universalQuantification;
	}

	
	
	@Override
	public void createClausesList(Set<MyPredicate> clauses) {
		clauses.add(this);
	}

	
	
	@Override
	public Set<String> getVariables() {
		MyPredicate implication = MyPredicateFactory.convertPredicate(universalQuantification.getImplication());
		Set<String> variables = implication.getVariables();
		variables.removeAll(getIdentifiers());
		return variables;
	}

	
	
	@Override
	public String toString() {
		StringBuffer universalQuant = new StringBuffer("");
		universalQuant.append("!(");
		List<String> identifiers = getIdentifiers();
		int idCounter = 1;
		for (String id : identifiers) {
			if(idCounter < identifiers.size()) {
				universalQuant.append(id + ",");
			} else {
				universalQuant.append(id);
			}
			idCounter++;
		}
		universalQuant.append(").");
		universalQuant.append(getImplication().toString());
		return universalQuant.toString();
	}
	
	
	
	private MyPredicate getImplication() {
		return MyPredicateFactory.convertPredicate(universalQuantification.getImplication());
	}

	
	
	private List<String> getIdentifiers() {
		List<String> identifiers = new ArrayList<String>();
		for (PExpression pExpression : universalQuantification.getIdentifiers()) {
			MyExpression myExpression = MyExpressionFactory.convertExpression(pExpression);
			identifiers.add(myExpression.toString());
		}
		return identifiers;
	}

	
	
	@Override
	public boolean isInterval() {
		return false;
	}
	
	
	
	@Override
	public boolean isTypingClause() {
		return false;
	}
	
}
